COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "HEAD.PUB[R,LES]" SOURCE
C00009 00003	.SS The First-Order Logic Solution
C00026 00004	.SS "Goals, Milestones, and Software"
C00041 00005	.CB Milestones
C00045 00006	.SS The Formal Reasoning Group.
C00048 00007	.bib
C00050 ENDMK
C⊗;
.REQUIRE "HEAD.PUB[R,LES]" SOURCE
.S FORMAL REASONING

\\pers John McCarthy, Richard Weyhrauch, William Glassmire, Michael Gordon,
Juan Bulnes, Robert Filman, Jerrold Ginsbarg, David Arnold, Arthur Thomas,
David Wilkins.

This includes the activities previously reported as proof-checking,
mathematical theory of computation, and representation theory.
They are combined in this proposal, because much the same people are
involved in all of them, and they require some of the same
developments of ideas and of software.

Before describing the present state of this work and what is
planned in the next two years, it seems desirable to explain our
conception of the problems involved in this area,
since this is perhaps the Laboratory's major
effort in the theoretical side of artificial intelligence.

.SS A Historical Perspective

There are two ways to approach the problem of designing intelligent systems.
The first, straightforward programming of specific intellectual tasks,
was explored extensively during the past decade of research in
artificial intelligence.  Typical problems which were studied include
playing various games, program verification, and proving theorems in
geometry.  The difficulty with this approach is that there is no natural
common framework in which to formulate the problems, so that one
is left with a large collection of clever but generally incompatible
ad hoc programs.

The second approach is to design a general intelligence system, able to
solve various classes of problems.  Typical of these efforts is the
General Problem Solver of Newell and Simon.  These efforts met with
only limited success.  An important reason for this failure is that
many problems can be represented to these programs only in a very awkward
fashion.

An analysis of the programs developed above has revealed an essential
difficulty of the artificial intelligence problem.  One explanation is
given in [McCarthy and Hayes], which divides the
problem into a %2heuristic%1 part and an %2epistemological%1 part.
The heuristic part, which
essentially involves methods of searching spaces of possibilities for the
solution to a specific problem, is reasonably well understood as a result
of the work described above.  In both the above approaches, the limiting
factor is the techniques available for expressing the information to the 
computer -- that is, the epistemological part of the problem.

We are studying the epistemological problem by building software to
represent human reasoning processes.   We call this system FOL.  It
does not yet address the question of how people %2find%* the answers
to questions, but only tries to represent inside a computer some 
human solutions to a wide variety of problems.  We
thus refer to FOL as a proof-checker (or more correctly a 
reasoning_checker) as opposed to a proof finder or theorem-prover.
There are several reasons for choosing to build a proof-checker, as 
opposed to a theorem-prover:

.bs
 (a) Formal [i.e., mechanizable] systems capable of %2expressing%*
     all known mathematical reasoning are available. This means that
     in the domain of mathematics a practically useful proof-checker
     is within realization, whereas a theorem-prover capable of 
     creative mathematical activity is a considerable way off.

 (b) Since proof-checkers and theorem-provers require the same 
     expressive capabilities, the epistemological problem can be
     studied just as well by building a proof-checker.

 (c) For many applications, e.g., correctness proofs for programs,
     a proof-checker will serve as well as a theorem-prover.

 (d) An %2a priori%1 introspective analysis is necessary to decide
     exactly what reasoning principles to incorporate into a theorem-
     prover.  We hope that formalizing many examples of human reasoning
     will reveal what principles people actually use in both ordinary
     and formal reasoning.  These %2may%1 then be designed into an 
     effective intelligent system.
.end

At present the proof-checker we are building has three main areas of
application:  proofs of mathematical theorems, verifying the correctness 
of hardware and software, and the representation of common sense reasoning.  
.SS The First-Order Logic Solution

The %3Formal Reasoning Group's%1 approach to the epistemological problem 
is based on first-order logic, by which we mean both the syntactic and 
semantic theory of the first order predicate calculus.  The predicate 
calculus is the language used in the formal systems mentioned above which 
are adequate to express mathematical reasoning.  The semantic component of 
first-order logic defines the correspondence between the syntatic
constructs of the formal languages and the mathematical objects they 
describe.  E.g., the symbol "+" in a formal system is usually declared 
to correspond to ordinary addition.

Scientists have traditionally regarded mathematical arguments as the 
ultimate in formal reasoning.  Since the predicate calculus has had 
striking theoretical success in representing mathematics, computer
scientists have used the predicate calculus before in attempts to build
intelligent systems.  These attempts have had three shortcomings:

.bs
 (a) To represent simple examples of ordinary human reasoning requires
     formal proofs of inordinate length.

 (b) These programs have had no %2uniform%1 way to express the
     correspondence between the formal system and the real world.

 (c) The commitment to a proof finding environment precluded 
     examining formalized examples of human reasoning.
.end

We have written FOL in a way which captures the computational part of 
first-order logic.  Our work on the problem of length of proofs is 
discussed in the following section.  Semantic attachment, FOL's solution 
to expressing the correspondence between languages and the objects they
talk about, is discussed immediately below.

The basic grammar of FOL is modeled on the natural deduction representation 
of the predicate calculus set forth in [Prawitz 1965].  The semantic analysis 
is contained in a group of subroutines, collectively christened semantic 
attachment, which are a computational version of the correspondence between 
the grammatical objects and the things being reasoned about.  These routines, 
permitting interaction between the program and the real world, are perhaps 
the most innovative feature of FOL.  We give several examples to illustrate 
its uses and discuss applications projects we think should be of interest 
to ARPA.

One example is analysis of photographs and diagrams.  Consider in particular
an aerial photograph of a city.  Let us assume that we have a tentative 
analysis of such a photograph, generated mechanically or by hand, which 
identifies certain picture elements as trucks, streets, buildings, and so 
on.  One way to check this analysis is to have a version of FOL which
contains information about cities, etc. in the form of an appropriate
theory in first-order logic.  Semantic attachment is then used to associate
the "recognizable" objects in the photo with their counterparts in the 
theory.  FOL can then be used to check the consistency of these associations
using its deductive ability.  E.g. if the analysis of some blob were to be 
a tree and it were found on something "recognized" as a baseball field, then
the semantic simplifier of FOL could report that something in the analysis
was incorrect.

As a second example, consider programs which operate on physical geometric 
objects and therefore need to analyze their properties.  Such a program can 
use the attachment routines to express facts about the shape and size of the 
objects involved.  As a concrete example, consider a program which manipulates
rectangles.  First, it can use FOL to describe what it means for one given
rectangle will fit inside a second rectangle.  Second it can describe to FOL
that it only needs to make some simple computations involving the lengths of 
the sides to decide if one will fit within another.  Rectangles could be 
seen by the program in many different ways: as ordinary input data, computed 
from a television picture of real cardboard rectangles, or perhaps calculated 
from the coordinates of the vertices.  Semantic Attachment of any of these 
procedures permits all these possibilities to be handled uniformly.  In
particular, if the program is the given any two rectangles in any of these 
ways FOL can be used to decide if one fits into the other.

A question similar in spirit to the preceding is to verify a program when 
its statement of correctness depends on knowing facts about the real 
world.  A simple example is that the records of an airline reservation 
system should correspond to reality; that is, a customer which the program 
thinks has a reservation should actually have one.  Another example is a
command and control system's list of airplanes, with their characteristics 
and locations, should agree with actual characteristics and locations.  A
proof that such a program meets its specifications will involve expressing 
facts about the real world.  

The latter examples show that programs of general interest may need a 
formalization of facts about the real world just to express (in a way 
understandable to a computer) their correctness. It is problems like these 
that we would eventually like to treat %2naturally.%1

Let us mention briefly our present conception of 
the research applications of FOL.  These fall into three separate areas.  The
most immediately accessible are the proofs in mathematics.  There
are several reasons for studying this problem. %2First%1, mathematics 
provides many easily available examples of long chains of 
human reasoning.  %2Second%1, the first-order logic representation 
of mathematics is the model on which FOL is based, 
so checking mathematical proofs is an obvious experimental
test.  %2Third%1, the formal notions used to represent mathematics are
well understood, so that correct axiomatizations for formalizing proofs
are easily obtained (though our experience shows that finding the most
usable axiomatization is still a problem).

The second area of applications is in correctness proofs, both for 
hardware implementations and for software.  There are three reasons 
for this: %2First%1, machine-checked correctness proofs are, in our 
opinion, the most promising practical technique in the long run for 
reducing the time necessary to get correct computer programs.  The 
reasons why this is so were elaborated in some of our earlier 
proposals to ARPA [Stanford 1969],
and pursuing this approach has been one of the major tasks of our
ARPA contract.  We have proved the correctness
of the ripple-carry algorithm for base 2 addition, and we will soon
prove the correctness of other algorithms, specifically the 
look-ahead carry algorithm.  %2Second%1, this domain complements pure 
mathematics nicely as a test of our ability to formalize reasoning, 
because there is still a substantial conceptual problem of determining 
what the right axioms are.  %2Third%1, AI in general is concerned with
reasoning that a strategy will solve a problem, and strategies are a
kind of program.  Therefore, the mathematics of program correctness
is likely to play an essential role in artificial intelligence as a
whole. 

Finally, we are using FOL to experiment with common sense reasoning. 
To study the problem of combining deductive reasoning with the 
representation of basic common sense facts, one needs a domain in
which there is a clear division between facts and reasoning.  Such a 
domain is provided by the chess problems mentioned above, which combine 
the step-by-step deductive reasoning characteristic of mathematical 
logic with facts obtained by observing the chessboard.  For example,
the first step in solving one of the problems is to observe that Black 
is in check.  A human being does not "prove" that Black is in check from 
axioms giving the positions of all the pieces; rather we just look at 
the board and see that Black is in check.  In contrast, the nature of
the deductive reasoning involved is exemplified by another part of 
the same problem; one shows that a 
White rook is a promoted pawn, a fact that certainly is not obvious
from the board.  

The important consideration in this problem is not the
domain of chess but the attempt to isolate the way in which computation
interacts with deduction.  FOL's semantic attachment feature models our 
observational ability by introducing a correspondence between 
certain predicate and function symbols in the logic and certain 
computable LISP functions and predicates.  When a statement 
involving these function symbols applied to known constants 
occurs, it can be verified by direct calculation using the corresponding LISP 
functions.  In the case of chess, we call the collection of LISP functions 
%2the chess eye%1.  We have explored what these functions are, but we don't 
have anything like a complete collection yet, because even the domains that 
these functions ought to have is unclear.  For example, some of them give 
answers when the position is only partially specified, and this property is 
essential to their use.  Therefore, we need to work with some useful class of 
partially specified positions.

Already the chess example has showed us improvements to formal logic
required to represent reasoning that involves observation.  We are
now ready to extend this work to include observations of the physical
world with a television camera.  This will be harder because there is
a great problem in expressing what humans know about the world of
scenes in a form usable by a computer, i.e. as FOL axioms and
attachments.

.SS "Goals, Milestones, and Software"

At present, the general goal of the %3Formal Reasoning Group%1 is to  
find out how to make it easier to express a many kinds of problems, both
mathematical and non-mathematical, in FOL.  We want to increase the
expressive capability of the basic FOL language and to make the actual
proof-checking procedure simpler and easier to use.  One way of achieving
the former is to modify the grammar to include other constructs, e.g.
conditional terms.  The latter involves discovering and implementing 
more powerful rules of inference, e.g. subgoaling or decision proceedures
for particular domains.  As explained above this is an essential 
prerequisite to machines actually being able to find solutions to these 
problems in an effecttive but general way.  In the intermediate term
we will produce an interface which will allow other programs to use
the expressive and deductive powers of FOL as they see fit.

Over the past several months we have demonstrated that it is possible 
to express many varieties of reasoning in FOL.  However, in practice a 
formalized proof is longer and more complicated than the corresponding 
informal proof.  Work is now in progress analyzing the formal proofs 
that have been done.  The proofs we have in hand are:

.bs
  (a)  The theorem "If p is a prime number and p divides the product a*b, 
       then p divides a or p divides b".  This theorem requires a knowledge
       of arithmetic.

  (b)  The theorem "If G is a finite group and S is a subgroup, then the
       order of S divides the order of G".  This theorem and the next use
       a significant part of set theory.

  (c)  The theorem "Let G be a countably infinite set of points, each 
       point being connected to every other by a thread, each thread being 
       red or black.  Then there is an infinite subset of these points
       such that the connecting threads within the subset are 
       all of the same color."

  (d)  Wilson's theorem "If p is a prime then (p-1)!≡1(mod p)."

  (e)  A correctness proof for a hardware implementation of
       the "ripple-carry" algorithm for base 2 addition.

  (f)  Two chess problems whose solution requires reasoning more complex 
       than a case-by-case analysis are being formalized.
.end

These proofs are at least as complicated (and in most cases more complicated)
than any proofs previously formulated for a machine to handle.  They are,
with the exception of (e), far beyond the capabilities of present day 
theorem-provers.  As mentioned in the introduction, we expect to extract
from these examples information about how we should configure computer
software to incorporate the reasoning principles involved in
problems of this complexity.  The results of this examination will influence 
how some of the features below will be developed.  

One problem in AI has been how does a program examine itself.  Suppose
you ask yourself why you believe something and you answer because I 
have convinced myself that it is true, i.e. I have proved it.  In 
order to make sense of this remark you must have some idea about
what it means to you for something to be a convincing argument.  This
is like being able to explain what a proof is.  The formal theory
theory which describes the grammar and the proofs in a theory T is
called the metatheory of T.  A large part of ordinary mathematics
and of common sense reasoning is actually metatheoretical.  Consider
the following commonplace examples:
.bs
 (a) Any description of how to look for a proof or to solve a problem
     is a metatheoretical statement.

 (b) The common three-dot notation for sequences, e.g. x1, x2, ... , xn,
     is a metatheoretical concept; one cannot express the notion of an
     arbitrary finite sequence directly in a first-order theory.

 (c) Axiom schemas are a third example.  In the past
     most treatments of first-order predicate calculus have been in
     resolution theorem provers.  Their inability to handle axiom schemas,
     i.e. to properly express the metatheory, has limited their capability
     to do proofs of arithmetic or set theory and thus excluded much of 
     mathematics.
.end
We intend to add to FOL the ability to express its metatheory, i.e., to talk
about its own proofs.  We refer to this as MFOL (for metaFOL).  

We will use MFOL to check some major metamathematics theorem of traditional
logic. At the moment we are considering Goedel's proof of the consistency
of the continuum hypothesis.  A word should perhaps be said here about
the value of this problem from ARPA's point of view.  
The overall objective of this work is to discover ways 
to represent reasoning using machines.  We believe that
the difficulties involved in representing deductive reasoning
will be the same for widely varying classes of problems, so
that it is primarily a matter of taste which problems we try 
to represent.  This particular problem is both difficult 
and representative.  We may never "finish" this project as we might 
learn all we think we can about building MFOL before its finished.

An especially important project is to represent in FOL the 
notions of set theory, which is the vehicle used by
first-order logic to express higher mathematics.  In
particular, set theory provides a framework for expressing
analysis, that branch of mathematics which includes 
trigonometry and the calculus.  A proof of the correctness
of a program for computing satellite trajectories (or more
simply, for computing sines and cosines) can only be expressed
in analysis.  There are several alternative axiomatizations
known for set theory, and part of this project is to choose
the most suitable for formalization in FOL.  

The above projects are designed to allow us to study theories,
i.e. formal systems, that at a theoretical (although not practical) 
level have well understood representations to study.  In addition we 
will investigate how these concepts actually work in areas for which 
the representation of knowledge or the reasoning that is done is still 
in question.  As mentioned above, chess problems have been an 
extremely useful vehicle for studying the interplay between formal 
proofs and the semantic attachment mechanism of FOL in a non-mathematical
area.  It should be pointed out that the use of chess was not for the
purpose of building software to play a game of chess, but rather to
study how proofs can be represented.  Thus it is a test case for more
real world applications of semantic attachment.  We will explore several 
aspects of the use of FOL in reasoning about the actual physical world --
the representations of physical structure, visual appearance, and some 
causal notions.  The semantic attachment feature will permit us
to connect the FOL reasoning mechanism with sensory 
apparatus (a TV camera). For example, a user may attach 
to an FOL term, representing the distance from one object 
to another, a vision program which can calculate the distance 
by examining a sequence of TV pictures.  We are presently
working on FOL axiomatizations for various geometries relevant 
to visual perception and visuo-motor tasks, e.g. projective 
geometry and the geometry of solids. Again, semantic attachment
will be utilized to define algebraic representations of geometric 
notions and use algebraic computations to supplement 
purely geometric reasoning.  We will also need to study 
how to translate the concepts of a geometry based on perceptions 
of space into classical Euclidean geometry of physical space.
The grand culmination will be a proof of the correctness of 
a strategy for a physical manipulation and assembly task.  
This differs from a practical assembly program in that
we are trying to express in a formal language much 
of the physical intuition which is at present 
coded into assembly programs in an ad hoc way.  

A form of Dana Scott's logic for computable functions will be axiomatized
in the predicate calculus in a form usable in FOL.  The proofs about 
programs which have been carried out in the specialized system LCF will 
thus be expressible in FOL.  Since LCF does not include quantification 
rules or set theoretic axioms, the FOL system will allow simpler proofs 
of more assertions.  

A notion of abstract pattern that is a generalization of
linguistic patterns will be further developed and applied to 
chess temporal and spatial patterns.  This will develop our 
understanding of the patterns used in human reasoning.  We
shall also apply it to describing the relations among objects
on a table and their two dimensional projections in a TV camera
image.  
.CB Milestones

⊗ September 1975: Semantic attachment will be made compatible with the full 
many sorted logic of FOL.

⊗ October 1975: An experiment using semantic attachment together with a TV 
camera will be designed.

⊗ October 1975: A suitable axiomatization of set theory will be expressed in 
FOL.

⊗ November 1975: A form of Dana Scott's logic for computable functions 
  will be axiomatized in the predicate calculus in a form usable in FOL.

⊗ January 1976: A notion of abstract pattern that is a generalization of
linguistic patterns will be developed and applied to temporal and spatial 
patterns.  

⊗ February 1976: An initial version of MFOL will be implemented.

⊗ August 1976: The representations of physical concepts discussed
above will be expressed in FOL.  An experiment using a TV camera 
together with FOL will be finished.

⊗ September 1976: Abstract patterns will be applied to describe
the relations among objects on a table and their two dimensional 
projections in a TV camera image.

.CB Software

To accomplish these goals will require several modifications and
additions to the present FOL software.  The code will be written
in pure LISP (easily translatable into INTERLISP) and available
for use at other sites on the ARPA net.  Several other researchers
have already expressed interest in using the program.

The following software will be completed during this contract:
.bc
⊗ The semantic attachment mechanism.  
⊗ A preliminary version of MFOL.
⊗ A method of specifying goals and creating subgoals.
⊗ A decision procedure for monadic predicate logic.
⊗ A rule of inference allowing convenient manipulation of quantifiers.
⊗ The ability of users to make definitions.
⊗ The ability of users to create theorems.
⊗ An interface of FOL to other LISP programs.
.end

These are not included in the section on milestones as the exact order
in which they will be done is not yet decided, so no specific dates 
could be assigned to most of them.
.SS The Formal Reasoning Group.

John McCarthy is Professor of Computer Science and has worked in the area
of formal reasoning applied to computer science and artificial intelligence
since 1957.
He is working on the translation of the Scott theory in FOL, on the expression
of chess reasoning in FOL, and on a formalism for generalized patterns again
using first order logic.

Richard Weyhrauch is Research Associate in Computer Science,
has a PhD from Stanford in mathematical logic and has worked on mathematical
theory of computation and the development of proof-checkers.  He is in charge
of the work on FOL.

Bill Glassmire is Research Associate in Computer Science,
has joined the group recently, is also a Stanford PhD in mathematical logic.
Weyhrauch and Glassmire are extending FOL and applying it to problems in
mathematics and mathematical theory of computation.

Michael Gordon has a PhD in computer science from the University of Edinburgh.
His thesis was on reasoning about a semantics and implementation of pure
LISP within the Scott-Strachey framework.
He will pursue the formalization of the interactive and machine oriented aspects
of LISP.

Arthur Thomas is a graduate student in psychology, has worked on FOL, and is
interested in application of FOL to reasoning about
projective geometry and to visually perceived scenes and other real world
phenomena.
Juan Bulnes is studying combinatorial proofs in FOL.
Robert Filman is working on expressing chess reasoning in FOL.
David Arnold is applying FOL to set theoretical problems.
David Wilkins is working on abstract patterns.
.bib

[McCarthy 1959] John McCarthy, "Programs with Common Sense", <Proc. Int. Conf.
on Mechanisation of Thought Processes>, Teddington, England, National Physical
Laboratory, 1959.

[McCarthy 1963] John McCarthy, "A Basis for a Mathematical Theory of Computation",
in  Biaffort, P., and Herschberg, D., (eds.), <Computer Programming and Formal
Systems,> North-Holland, Amsterdam, 1963.

[McCarthy and Hayes]  John McCarthy and Patrick Hayes, "Some Philosophical Problems from the
Standpoint of Artificial Intelligence", AIM-73, November 1968; also in
D. Michie (ed.), <Machine Intelligence,> American Elsevier, New York, 1969.

[Prawitz 1965] Dag Prawitz, <Natural Deduction,> Almqvist & Wiksell, Stockholm, 1965.

[Stanford 1969], Stanford University, "Proposal for Continuation of the
Stanford Artificial Intelligence Project and the Heuristic Dendral Project",
proposal to ARPA, June 1969.

.end